purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
↳ QTRS
↳ DependencyPairsProof
purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
PURGE(.(x, y)) → REMOVE(x, y)
REMOVE(x, .(y, z)) → REMOVE(x, z)
PURGE(.(x, y)) → PURGE(remove(x, y))
purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
PURGE(.(x, y)) → REMOVE(x, y)
REMOVE(x, .(y, z)) → REMOVE(x, z)
PURGE(.(x, y)) → PURGE(remove(x, y))
purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
REMOVE(x, .(y, z)) → REMOVE(x, z)
purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REMOVE(x, .(y, z)) → REMOVE(x, z)
The value of delta used in the strict ordering is 1.
POL(REMOVE(x1, x2)) = (4)x_2
POL(.(x1, x2)) = 1/4 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
PURGE(.(x, y)) → PURGE(remove(x, y))
purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PURGE(.(x, y)) → PURGE(remove(x, y))
The value of delta used in the strict ordering is 16.
POL(remove(x1, x2)) = 0
POL(if(x1, x2, x3)) = 0
POL(=(x1, x2)) = 0
POL(.(x1, x2)) = 4 + (4)x_1
POL(nil) = 0
POL(PURGE(x1)) = (4)x_1
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))